YES 2.365
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ LR
mainModule List
| ((group :: [Ordering] -> [[Ordering]]) :: [Ordering] -> [[Ordering]]) |
module List where
| import qualified Maybe import qualified Prelude
|
| group :: Eq a => [a] -> [[a]]
|
| groupBy :: (a -> a -> Bool) -> [a] -> [[a]]
groupBy | _ [] | = | [] |
groupBy | eq (x : xs) | = |
(x : ys) : groupBy eq zs | where |
|
|
|
module Maybe where
| import qualified List import qualified Prelude
|
Lambda Reductions:
The following Lambda expression
\(_,zs)→zs
is transformed to
The following Lambda expression
\(ys,_)→ys
is transformed to
The following Lambda expression
\(_,zs)→zs
is transformed to
The following Lambda expression
\(ys,_)→ys
is transformed to
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
mainModule List
| ((group :: [Ordering] -> [[Ordering]]) :: [Ordering] -> [[Ordering]]) |
module List where
| import qualified Maybe import qualified Prelude
|
| group :: Eq a => [a] -> [[a]]
|
| groupBy :: (a -> a -> Bool) -> [a] -> [[a]]
groupBy | _ [] | = | [] |
groupBy | eq (x : xs) | = |
(x : ys) : groupBy eq zs | where |
|
|
|
module Maybe where
| import qualified List import qualified Prelude
|
Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern
xs@(wu : wv)
is replaced by the following term
wu : wv
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule List
| ((group :: [Ordering] -> [[Ordering]]) :: [Ordering] -> [[Ordering]]) |
module List where
| import qualified Maybe import qualified Prelude
|
| group :: Eq a => [a] -> [[a]]
|
| groupBy :: (a -> a -> Bool) -> [a] -> [[a]]
groupBy | vw [] | = | [] |
groupBy | eq (x : xs) | = |
(x : ys) : groupBy eq zs | where |
|
|
|
module Maybe where
| import qualified List import qualified Prelude
|
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
The following Function with conditions
span | p [] | = ([],[]) |
span | p (wu : wv) | |
is transformed to
span | p [] | = span3 p [] |
span | p (wu : wv) | = span2 p (wu : wv) |
span2 | p (wu : wv) | =
span1 p wu wv (p wu) |
where |
span0 | p wu wv True | = ([],wu : wv) |
|
|
span1 | p wu wv True | = (wu : ys,zs) |
span1 | p wu wv False | = span0 p wu wv otherwise |
|
| |
| |
| |
| |
| |
|
span3 | p [] | = ([],[]) |
span3 | xv xw | = span2 xv xw |
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
mainModule List
| ((group :: [Ordering] -> [[Ordering]]) :: [Ordering] -> [[Ordering]]) |
module List where
| import qualified Maybe import qualified Prelude
|
| group :: Eq a => [a] -> [[a]]
|
| groupBy :: (a -> a -> Bool) -> [a] -> [[a]]
groupBy | vw [] | = | [] |
groupBy | eq (x : xs) | = |
(x : ys) : groupBy eq zs | where |
|
|
|
module Maybe where
| import qualified List import qualified Prelude
|
Let/Where Reductions:
The bindings of the following Let/Where expression
(x : ys) : groupBy eq zs |
where | |
| |
| |
| |
| |
are unpacked to the following functions on top level
groupByYs0 | xx xy xz (ys,vx) | = ys |
groupByVv10 | xx xy xz | = span (xx xy) xz |
groupByZs0 | xx xy xz (vy,zs) | = zs |
groupByYs | xx xy xz | = groupByYs0 xx xy xz (groupByVv10 xx xy xz) |
groupByZs | xx xy xz | = groupByZs0 xx xy xz (groupByVv10 xx xy xz) |
The bindings of the following Let/Where expression
span1 p wu wv (p wu) |
where |
span0 | p wu wv True | = ([],wu : wv) |
|
|
span1 | p wu wv True | = (wu : ys,zs) |
span1 | p wu wv False | = span0 p wu wv otherwise |
|
| |
| |
| |
| |
| |
are unpacked to the following functions on top level
span2Zs | yu yv | = span2Zs1 yu yv (span2Vu43 yu yv) |
span2Ys1 | yu yv (ys,wx) | = ys |
span2Vu43 | yu yv | = span yu yv |
span2Zs1 | yu yv (ww,zs) | = zs |
span2Span1 | yu yv p wu wv True | = (wu : span2Ys yu yv,span2Zs yu yv) |
span2Span1 | yu yv p wu wv False | = span2Span0 yu yv p wu wv otherwise |
span2Span0 | yu yv p wu wv True | = ([],wu : wv) |
span2Ys | yu yv | = span2Ys1 yu yv (span2Vu43 yu yv) |
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
mainModule List
| (group :: [Ordering] -> [[Ordering]]) |
module List where
| import qualified Maybe import qualified Prelude
|
| group :: Eq a => [a] -> [[a]]
|
| groupBy :: (a -> a -> Bool) -> [a] -> [[a]]
groupBy | vw [] | = | [] |
groupBy | eq (x : xs) | = | (x : groupByYs eq x xs) : groupBy eq (groupByZs eq x xs) |
|
|
groupByVv10 | xx xy xz | = | span (xx xy) xz |
|
|
groupByYs | xx xy xz | = | groupByYs0 xx xy xz (groupByVv10 xx xy xz) |
|
|
groupByYs0 | xx xy xz (ys,vx) | = | ys |
|
|
groupByZs | xx xy xz | = | groupByZs0 xx xy xz (groupByVv10 xx xy xz) |
|
|
groupByZs0 | xx xy xz (vy,zs) | = | zs |
|
module Maybe where
| import qualified List import qualified Prelude
|
Haskell To QDPs
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_span2Zs(:(GT, yw3111)) → new_span2Zs(yw3111)
new_span2Ys(:(GT, yw3111)) → new_span2Zs(yw3111)
new_span2Ys(:(GT, yw3111)) → new_span2Ys(yw3111)
new_span2Zs(:(GT, yw3111)) → new_span2Ys(yw3111)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_span2Ys(:(GT, yw3111)) → new_span2Ys(yw3111)
The graph contains the following edges 1 > 1
- new_span2Ys(:(GT, yw3111)) → new_span2Zs(yw3111)
The graph contains the following edges 1 > 1
- new_span2Zs(:(GT, yw3111)) → new_span2Ys(yw3111)
The graph contains the following edges 1 > 1
- new_span2Zs(:(GT, yw3111)) → new_span2Zs(yw3111)
The graph contains the following edges 1 > 1
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_span2Zs0(:(EQ, yw3111)) → new_span2Ys0(yw3111)
new_span2Ys0(:(EQ, yw3111)) → new_span2Zs0(yw3111)
new_span2Ys0(:(EQ, yw3111)) → new_span2Ys0(yw3111)
new_span2Zs0(:(EQ, yw3111)) → new_span2Zs0(yw3111)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_span2Ys0(:(EQ, yw3111)) → new_span2Zs0(yw3111)
The graph contains the following edges 1 > 1
- new_span2Ys0(:(EQ, yw3111)) → new_span2Ys0(yw3111)
The graph contains the following edges 1 > 1
- new_span2Zs0(:(EQ, yw3111)) → new_span2Zs0(yw3111)
The graph contains the following edges 1 > 1
- new_span2Zs0(:(EQ, yw3111)) → new_span2Ys0(yw3111)
The graph contains the following edges 1 > 1
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_span2Zs1(:(LT, yw3111)) → new_span2Zs1(yw3111)
new_span2Ys1(:(LT, yw3111)) → new_span2Zs1(yw3111)
new_span2Zs1(:(LT, yw3111)) → new_span2Ys1(yw3111)
new_span2Ys1(:(LT, yw3111)) → new_span2Ys1(yw3111)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_span2Zs1(:(LT, yw3111)) → new_span2Zs1(yw3111)
The graph contains the following edges 1 > 1
- new_span2Zs1(:(LT, yw3111)) → new_span2Ys1(yw3111)
The graph contains the following edges 1 > 1
- new_span2Ys1(:(LT, yw3111)) → new_span2Zs1(yw3111)
The graph contains the following edges 1 > 1
- new_span2Ys1(:(LT, yw3111)) → new_span2Ys1(yw3111)
The graph contains the following edges 1 > 1
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
Q DP problem:
The TRS P consists of the following rules:
new_groupBy(:(yw30, yw31)) → new_groupBy(new_groupByZs0(yw30, yw31))
The TRS R consists of the following rules:
new_span2Zs2(:(EQ, yw3111)) → :(EQ, yw3111)
new_span2Zs4([]) → []
new_groupByZs0(GT, :(GT, yw311)) → new_span2Zs2(yw311)
new_groupByZs0(LT, :(GT, yw311)) → :(GT, yw311)
new_span2Zs3(:(EQ, yw3111)) → new_span2Zs12(yw3111, new_span2Ys3(yw3111), new_span2Zs3(yw3111))
new_span2Ys3([]) → []
new_span2Ys3(:(GT, yw3111)) → []
new_span2Ys12(yw3111, yw7, yw6) → :(EQ, yw7)
new_span2Ys3(:(EQ, yw3111)) → new_span2Ys12(yw3111, new_span2Ys3(yw3111), new_span2Zs3(yw3111))
new_span2Zs12(yw3111, yw13, yw12) → yw12
new_groupByZs0(GT, :(EQ, yw311)) → :(EQ, yw311)
new_span2Zs3(:(GT, yw3111)) → :(GT, yw3111)
new_groupByZs0(yw30, []) → []
new_groupByZs0(EQ, :(LT, yw311)) → :(LT, yw311)
new_span2Ys4(:(EQ, yw3111)) → []
new_groupByZs0(EQ, :(EQ, yw311)) → new_span2Zs3(yw311)
new_span2Zs4(:(EQ, yw3111)) → :(EQ, yw3111)
new_span2Ys2(:(EQ, yw3111)) → []
new_span2Zs4(:(LT, yw3111)) → new_span2Zs10(yw3111, new_span2Ys4(yw3111), new_span2Zs4(yw3111))
new_groupByZs0(LT, :(LT, yw311)) → new_span2Zs4(yw311)
new_groupByZs0(LT, :(EQ, yw311)) → :(EQ, yw311)
new_span2Ys2([]) → []
new_span2Zs4(:(GT, yw3111)) → :(GT, yw3111)
new_span2Ys2(:(GT, yw3111)) → new_span2Ys10(yw3111, new_span2Ys2(yw3111), new_span2Zs2(yw3111))
new_span2Zs11(yw3111, yw15, yw14) → yw14
new_span2Zs3([]) → []
new_groupByZs0(EQ, :(GT, yw311)) → :(GT, yw311)
new_span2Zs2([]) → []
new_span2Ys3(:(LT, yw3111)) → []
new_span2Ys4(:(LT, yw3111)) → new_span2Ys11(yw3111, new_span2Ys4(yw3111), new_span2Zs4(yw3111))
new_span2Ys11(yw3111, yw5, yw4) → :(LT, yw5)
new_span2Zs2(:(LT, yw3111)) → :(LT, yw3111)
new_span2Ys4([]) → []
new_span2Zs3(:(LT, yw3111)) → :(LT, yw3111)
new_groupByZs0(GT, :(LT, yw311)) → :(LT, yw311)
new_span2Ys10(yw3111, yw9, yw8) → :(GT, yw9)
new_span2Zs2(:(GT, yw3111)) → new_span2Zs11(yw3111, new_span2Ys2(yw3111), new_span2Zs2(yw3111))
new_span2Ys2(:(LT, yw3111)) → []
new_span2Zs10(yw3111, yw11, yw10) → yw10
new_span2Ys4(:(GT, yw3111)) → []
The set Q consists of the following terms:
new_span2Ys2([])
new_span2Zs12(x0, x1, x2)
new_groupByZs0(GT, :(EQ, x0))
new_groupByZs0(EQ, :(LT, x0))
new_span2Zs11(x0, x1, x2)
new_groupByZs0(EQ, :(EQ, x0))
new_span2Ys10(x0, x1, x2)
new_span2Ys3(:(EQ, x0))
new_span2Ys4(:(EQ, x0))
new_groupByZs0(GT, :(LT, x0))
new_span2Ys3([])
new_span2Ys2(:(EQ, x0))
new_groupByZs0(LT, :(LT, x0))
new_span2Ys3(:(LT, x0))
new_span2Zs4(:(GT, x0))
new_span2Ys2(:(GT, x0))
new_span2Ys4([])
new_span2Zs4(:(LT, x0))
new_span2Ys12(x0, x1, x2)
new_groupByZs0(GT, :(GT, x0))
new_span2Zs3(:(GT, x0))
new_groupByZs0(LT, :(GT, x0))
new_span2Zs10(x0, x1, x2)
new_span2Zs3(:(LT, x0))
new_span2Zs3([])
new_span2Zs2(:(EQ, x0))
new_span2Ys4(:(LT, x0))
new_groupByZs0(x0, [])
new_span2Ys4(:(GT, x0))
new_span2Ys3(:(GT, x0))
new_span2Zs3(:(EQ, x0))
new_span2Zs4([])
new_span2Zs2(:(GT, x0))
new_span2Ys2(:(LT, x0))
new_span2Zs2([])
new_groupByZs0(LT, :(EQ, x0))
new_span2Zs2(:(LT, x0))
new_span2Ys11(x0, x1, x2)
new_groupByZs0(EQ, :(GT, x0))
new_span2Zs4(:(EQ, x0))
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].
The following pairs can be oriented strictly and are deleted.
new_groupBy(:(yw30, yw31)) → new_groupBy(new_groupByZs0(yw30, yw31))
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25]:
POL(:(x1, x2)) = 1 + x2
POL(EQ) = 0
POL(GT) = 0
POL(LT) = 0
POL([]) = 0
POL(new_groupBy(x1)) = x1
POL(new_groupByZs0(x1, x2)) = x2
POL(new_span2Ys10(x1, x2, x3)) = 1 + x2
POL(new_span2Ys11(x1, x2, x3)) = 1 + x2
POL(new_span2Ys12(x1, x2, x3)) = 1 + x2
POL(new_span2Ys2(x1)) = 1 + x1
POL(new_span2Ys3(x1)) = x1
POL(new_span2Ys4(x1)) = x1
POL(new_span2Zs10(x1, x2, x3)) = x3
POL(new_span2Zs11(x1, x2, x3)) = x3
POL(new_span2Zs12(x1, x2, x3)) = 1 + x3
POL(new_span2Zs2(x1)) = x1
POL(new_span2Zs3(x1)) = x1
POL(new_span2Zs4(x1)) = x1
The following usable rules [17] were oriented:
new_span2Zs2(:(LT, yw3111)) → :(LT, yw3111)
new_span2Ys4(:(EQ, yw3111)) → []
new_groupByZs0(GT, :(LT, yw311)) → :(LT, yw311)
new_span2Ys2(:(GT, yw3111)) → new_span2Ys10(yw3111, new_span2Ys2(yw3111), new_span2Zs2(yw3111))
new_span2Ys3(:(GT, yw3111)) → []
new_span2Ys4([]) → []
new_span2Zs3(:(GT, yw3111)) → :(GT, yw3111)
new_span2Zs4(:(GT, yw3111)) → :(GT, yw3111)
new_span2Zs2(:(GT, yw3111)) → new_span2Zs11(yw3111, new_span2Ys2(yw3111), new_span2Zs2(yw3111))
new_span2Zs3(:(EQ, yw3111)) → new_span2Zs12(yw3111, new_span2Ys3(yw3111), new_span2Zs3(yw3111))
new_span2Ys3(:(LT, yw3111)) → []
new_span2Zs3(:(LT, yw3111)) → :(LT, yw3111)
new_groupByZs0(yw30, []) → []
new_span2Zs3([]) → []
new_groupByZs0(LT, :(LT, yw311)) → new_span2Zs4(yw311)
new_groupByZs0(LT, :(GT, yw311)) → :(GT, yw311)
new_span2Ys11(yw3111, yw5, yw4) → :(LT, yw5)
new_groupByZs0(EQ, :(LT, yw311)) → :(LT, yw311)
new_span2Ys4(:(GT, yw3111)) → []
new_span2Zs4(:(LT, yw3111)) → new_span2Zs10(yw3111, new_span2Ys4(yw3111), new_span2Zs4(yw3111))
new_groupByZs0(EQ, :(GT, yw311)) → :(GT, yw311)
new_groupByZs0(GT, :(GT, yw311)) → new_span2Zs2(yw311)
new_groupByZs0(GT, :(EQ, yw311)) → :(EQ, yw311)
new_span2Zs10(yw3111, yw11, yw10) → yw10
new_span2Ys3([]) → []
new_span2Zs2([]) → []
new_span2Zs2(:(EQ, yw3111)) → :(EQ, yw3111)
new_span2Ys2(:(LT, yw3111)) → []
new_groupByZs0(EQ, :(EQ, yw311)) → new_span2Zs3(yw311)
new_groupByZs0(LT, :(EQ, yw311)) → :(EQ, yw311)
new_span2Zs4(:(EQ, yw3111)) → :(EQ, yw3111)
new_span2Ys2([]) → []
new_span2Zs4([]) → []
new_span2Zs12(yw3111, yw13, yw12) → yw12
new_span2Ys3(:(EQ, yw3111)) → new_span2Ys12(yw3111, new_span2Ys3(yw3111), new_span2Zs3(yw3111))
new_span2Ys4(:(LT, yw3111)) → new_span2Ys11(yw3111, new_span2Ys4(yw3111), new_span2Zs4(yw3111))
new_span2Ys10(yw3111, yw9, yw8) → :(GT, yw9)
new_span2Zs11(yw3111, yw15, yw14) → yw14
new_span2Ys2(:(EQ, yw3111)) → []
new_span2Ys12(yw3111, yw7, yw6) → :(EQ, yw7)
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
Q DP problem:
P is empty.
The TRS R consists of the following rules:
new_span2Zs2(:(EQ, yw3111)) → :(EQ, yw3111)
new_span2Zs4([]) → []
new_groupByZs0(GT, :(GT, yw311)) → new_span2Zs2(yw311)
new_groupByZs0(LT, :(GT, yw311)) → :(GT, yw311)
new_span2Zs3(:(EQ, yw3111)) → new_span2Zs12(yw3111, new_span2Ys3(yw3111), new_span2Zs3(yw3111))
new_span2Ys3([]) → []
new_span2Ys3(:(GT, yw3111)) → []
new_span2Ys12(yw3111, yw7, yw6) → :(EQ, yw7)
new_span2Ys3(:(EQ, yw3111)) → new_span2Ys12(yw3111, new_span2Ys3(yw3111), new_span2Zs3(yw3111))
new_span2Zs12(yw3111, yw13, yw12) → yw12
new_groupByZs0(GT, :(EQ, yw311)) → :(EQ, yw311)
new_span2Zs3(:(GT, yw3111)) → :(GT, yw3111)
new_groupByZs0(yw30, []) → []
new_groupByZs0(EQ, :(LT, yw311)) → :(LT, yw311)
new_span2Ys4(:(EQ, yw3111)) → []
new_groupByZs0(EQ, :(EQ, yw311)) → new_span2Zs3(yw311)
new_span2Zs4(:(EQ, yw3111)) → :(EQ, yw3111)
new_span2Ys2(:(EQ, yw3111)) → []
new_span2Zs4(:(LT, yw3111)) → new_span2Zs10(yw3111, new_span2Ys4(yw3111), new_span2Zs4(yw3111))
new_groupByZs0(LT, :(LT, yw311)) → new_span2Zs4(yw311)
new_groupByZs0(LT, :(EQ, yw311)) → :(EQ, yw311)
new_span2Ys2([]) → []
new_span2Zs4(:(GT, yw3111)) → :(GT, yw3111)
new_span2Ys2(:(GT, yw3111)) → new_span2Ys10(yw3111, new_span2Ys2(yw3111), new_span2Zs2(yw3111))
new_span2Zs11(yw3111, yw15, yw14) → yw14
new_span2Zs3([]) → []
new_groupByZs0(EQ, :(GT, yw311)) → :(GT, yw311)
new_span2Zs2([]) → []
new_span2Ys3(:(LT, yw3111)) → []
new_span2Ys4(:(LT, yw3111)) → new_span2Ys11(yw3111, new_span2Ys4(yw3111), new_span2Zs4(yw3111))
new_span2Ys11(yw3111, yw5, yw4) → :(LT, yw5)
new_span2Zs2(:(LT, yw3111)) → :(LT, yw3111)
new_span2Ys4([]) → []
new_span2Zs3(:(LT, yw3111)) → :(LT, yw3111)
new_groupByZs0(GT, :(LT, yw311)) → :(LT, yw311)
new_span2Ys10(yw3111, yw9, yw8) → :(GT, yw9)
new_span2Zs2(:(GT, yw3111)) → new_span2Zs11(yw3111, new_span2Ys2(yw3111), new_span2Zs2(yw3111))
new_span2Ys2(:(LT, yw3111)) → []
new_span2Zs10(yw3111, yw11, yw10) → yw10
new_span2Ys4(:(GT, yw3111)) → []
The set Q consists of the following terms:
new_span2Ys2([])
new_span2Zs12(x0, x1, x2)
new_groupByZs0(GT, :(EQ, x0))
new_groupByZs0(EQ, :(LT, x0))
new_span2Zs11(x0, x1, x2)
new_groupByZs0(EQ, :(EQ, x0))
new_span2Ys10(x0, x1, x2)
new_span2Ys3(:(EQ, x0))
new_span2Ys4(:(EQ, x0))
new_groupByZs0(GT, :(LT, x0))
new_span2Ys3([])
new_span2Ys2(:(EQ, x0))
new_groupByZs0(LT, :(LT, x0))
new_span2Ys3(:(LT, x0))
new_span2Zs4(:(GT, x0))
new_span2Ys2(:(GT, x0))
new_span2Ys4([])
new_span2Zs4(:(LT, x0))
new_span2Ys12(x0, x1, x2)
new_groupByZs0(GT, :(GT, x0))
new_span2Zs3(:(GT, x0))
new_groupByZs0(LT, :(GT, x0))
new_span2Zs10(x0, x1, x2)
new_span2Zs3(:(LT, x0))
new_span2Zs3([])
new_span2Zs2(:(EQ, x0))
new_span2Ys4(:(LT, x0))
new_groupByZs0(x0, [])
new_span2Ys4(:(GT, x0))
new_span2Ys3(:(GT, x0))
new_span2Zs3(:(EQ, x0))
new_span2Zs4([])
new_span2Zs2(:(GT, x0))
new_span2Ys2(:(LT, x0))
new_span2Zs2([])
new_groupByZs0(LT, :(EQ, x0))
new_span2Zs2(:(LT, x0))
new_span2Ys11(x0, x1, x2)
new_groupByZs0(EQ, :(GT, x0))
new_span2Zs4(:(EQ, x0))
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.